\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$), ${\it upd}$:update{-}spec(${\it ds}$;${\it da}$),\+
\\[0ex]$T$:Type, ${\it ks}$:Knd List, $a$:($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$)), $x$:Id.
\-\\[0ex]$\neg$$x$ $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ update{-}spec{-}decl(${\it upd}$;${\it ds}$)
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ $k$ $\in$ dom(${\it da}$))
\\[0ex]$\Rightarrow$ ecl{-}machine2($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it upd}$) $\parallel$ ecl{-}machine3(${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it snd}$)
\end{tabbing}